#include "common.h"
int main() {
	int result = false;

	Activity activity1;
	// strcpy(activity1.name, "zs");
	// activity1.shopId = 1;
	// activity1.on = 1;


	Activity activity2;
	// strcpy(activity2.name, "LS");
	// activity2.shopId = 1;
	// activity2.on = 1;

	// printRow_activity(&activity1,"init_1");
	klee_make_symbolic(&activity1, sizeof(activity1), "activity1");
	// printRow_activity(&activity1,"init_2");
	klee_assume(assume_fieldInList_activity_name(&activity1));
	klee_assume(assume_fieldInList_activity_shopId(&activity1));
	klee_assume(assume_fieldInList_activity_on(&activity1));
    
	klee_make_symbolic(&activity2, sizeof(activity2), "activity2");
	klee_assume(assume_fieldInList_activity_name(&activity2));
	klee_assume(assume_fieldInList_activity_shopId(&activity2));
	klee_assume(assume_fieldInList_activity_on(&activity2));
    
	// klee_make_symbolic(&activityTabCurId, sizeof(activityTabCurId), "activityTabCurId");
	// klee_make_symbolic(&activityTabCurIndex, sizeof(activityTabCurIndex), "activityTabCurIndex");
	// klee_make_symbolic(&activityTab, sizeof(activityTab), "activityTab");
	// klee_assume(isValidActivity(&activity));
	// klee_assume(internalCheckTableValidated_activity());
	// printRow_activity(&activity1,"before_api_save_row_activity");
	result = api_save_row_activity(&activity1);
	// printRow_activity(&activity1,"after_api_save_row_activity");
	assert(result == OK);
	
	// printRow_activity(&activity2,"before_api_save_row_activity");
	result = api_save_row_activity(&activity2);
	// printRow_activity(&activity2,"after_api_save_row_activity");
	assert(result == OK);

	// for(int i = 1; i < TableMaxRow-1; i++){

	// result = api_save_row_activity(&activity);
	// printf("result = %d\n", result);
	// assert(result == OK);
	// }
	return 0;
}
